# import idautils
# import idaapi
# import idc

# functions = [0x1193,0x11F2,0x1253,0x12B1,0x130D,0x136E,0x13CC,0x142A,0x148D,0x14EB,0x154B,0x15A9,0x160A,0x166C,0x16CC,0x172D,0x178C,0x17ED,0x184B,0x18AB,0x1909,0x196B,0x19C8,0x1A26,0x1A88,0x1AE6,0x1B44,0x1BA4,0x1C07,0x1C69,0x1CC9,0x1D07,0x1D46,0x1DA4,0x1E04,0x1E65,0x1EC8,0x1F26,0x1F84,0x1FE2,0x2042,0x207C,0x20DA,0x2132,0x2191,0x21EF,0x2249,0x22A7,0x2305,0x2365,0x23C8,0x2429,0x2489,0x24E7,0x2526,0x2586,0x25E2,0x2643,0x26A4,0x2706,0x2769,0x27C7,0x2829,0x2887,0x28E8,0x2946,0x29A8,0x2A09,0x2A6C,0x2ACD,0x2B2E,0x2B8C,0x2BEC,0x2C4A,0x2CA8,0x2D09,0x2D69,0x2DC9,0x2E2A,0x2E87,0x2EE8,0x2F46,0x2FA8,0x3003,0x306C,0x30CD,0x3129,0x318A,0x31E9,0x324A,0x32AC,0x330A,0x3364,0x33C5,0x3423,0x3484,0x34E4,0x3545]

# for i in functions:
#     func=idaapi.get_func(i)
#     cfunc = idaapi.decompile(func)
#     cond = str(idaapi.decompile(idaapi.get_func(i))).split("\n")[4].lstrip().rstrip()[24:-2].replace("*a1","a1[0]",-1).replace("*(char *)(a1 + ","a1[",-1).replace(")","]",-1).replace("a1","CHARS",-1)
#     comp = str(cfunc).split("\n")[5].lstrip().rstrip().split("!=")[1][:-1].lstrip().rstrip()
#     print("s.add({}=={})".format(cond, comp))

from z3 import *

charset = "abcdefghijklmnopqrstuvwxyz1234567890{_}"
CHARS =[Int("char_{}".format(x)) for x in range(32)]

def is_valid(c):
    return Or([c == ord(x) for x in charset])

s = Solver()
for i in range(5,28):
    s.add(is_valid(CHARS[i]))

s.add(CHARS[0]==ord("e"))
s.add(CHARS[1]==ord("v"))
s.add(CHARS[2]==ord("l"))
s.add(CHARS[3]==ord("z"))
s.add(CHARS[4]==ord("{"))
s.add(CHARS[-4]==ord("}"))
s.add(CHARS[-3]==ord("c"))
s.add(CHARS[-2]==ord("t"))
s.add(CHARS[-1]==ord("f"))

s.add(CHARS[29] + CHARS[12] * CHARS[1] + CHARS[9]==12125)
s.add(CHARS[12] + CHARS[12] * CHARS[8] - CHARS[4]==9775)
s.add(CHARS[26] + CHARS[1] - CHARS[21] + CHARS[11]==159)
s.add(CHARS[8] + CHARS[0] * CHARS[8] * CHARS[14]==480150)
s.add(CHARS[21] - CHARS[4] + CHARS[22] * CHARS[21]==5545)
s.add(CHARS[13] + CHARS[10] + CHARS[14] + CHARS[1]==311)
s.add(CHARS[8] - CHARS[17] - CHARS[1] + CHARS[30]==-9)
s.add(CHARS[26] - CHARS[21] - CHARS[26] * CHARS[13]==-4903)
s.add(CHARS[13] - CHARS[18] - CHARS[26] + CHARS[29]==91)
s.add(CHARS[12] + CHARS[15] * CHARS[4] + CHARS[17]==14473)
s.add(CHARS[27] + CHARS[9] - CHARS[4] + CHARS[12]==201)
s.add(CHARS[6] * CHARS[8] - CHARS[8] + CHARS[3]==4681)
s.add(CHARS[20] - CHARS[31] - CHARS[8] - CHARS[31]==-206)
s.add(CHARS[17] * CHARS[8] * CHARS[15] - CHARS[31]==1170106)
s.add(CHARS[20] - CHARS[29] + CHARS[4] - CHARS[3]==-3)
s.add(CHARS[11] + CHARS[29] * CHARS[13] + CHARS[1]==9622)
s.add(CHARS[12] - CHARS[23] + CHARS[18] - CHARS[4]==-67)
s.add(CHARS[2] - CHARS[4] - CHARS[5] + CHARS[30]==-9)
s.add(CHARS[5] + CHARS[20] * CHARS[20] + CHARS[24]==9188)
s.add(CHARS[7] + CHARS[11] + CHARS[2] + CHARS[29]==401)
s.add(CHARS[9] - CHARS[13] - CHARS[29] - CHARS[1]==-204)
s.add(CHARS[6] - CHARS[23] + CHARS[0] - CHARS[23]==-45)
s.add(CHARS[5] + CHARS[1] - CHARS[4] - CHARS[6]==57)
s.add(CHARS[31] * CHARS[23] + CHARS[29] * CHARS[3]==21972)
s.add(CHARS[22] + CHARS[25] + CHARS[16] + CHARS[31]==356)
s.add(CHARS[4] + CHARS[29] - CHARS[31] - CHARS[29]==21)
s.add(CHARS[23] + CHARS[11] * CHARS[24] + CHARS[22]==5395)
s.add(CHARS[30] * CHARS[2] - CHARS[14] - CHARS[15]==12363)
s.add(CHARS[13] - CHARS[17] - CHARS[20] - CHARS[14]==-153)
s.add(CHARS[28] + CHARS[24] + CHARS[16] - CHARS[29]==174)
s.add(CHARS[7] + CHARS[8]==192)
s.add(CHARS[16] * CHARS[1]==11210)
s.add(CHARS[12] + CHARS[5] - CHARS[28] - CHARS[12]==-15)
s.add(CHARS[16] + CHARS[29] + CHARS[2] * CHARS[22]==5702)
s.add(CHARS[30] - CHARS[12] + CHARS[29] + CHARS[26]==165)
s.add(CHARS[26] - CHARS[27] - CHARS[19] * CHARS[13]==-10989)
s.add(CHARS[11] + CHARS[20] - CHARS[25] + CHARS[23]==183)
s.add(CHARS[11] + CHARS[22] - CHARS[23] - CHARS[25]==-55)
s.add(CHARS[17] - CHARS[15] - CHARS[22] + CHARS[8]==34)
s.add(CHARS[11] - CHARS[10] * CHARS[14] * CHARS[4]==-295224)
s.add(CHARS[0] + CHARS[3]==223)
s.add(CHARS[17] - CHARS[22] - CHARS[26] + CHARS[30]==118)
s.add(CHARS[9] - CHARS[0] - CHARS[24] + CHARS[21]==63)
s.add(CHARS[28] + CHARS[2] * CHARS[22] + CHARS[11]==5732)
s.add(CHARS[22] - CHARS[13] - CHARS[12] + CHARS[1]==-27)
s.add(CHARS[18] + CHARS[30] - CHARS[0] + CHARS[20]==162)
s.add(CHARS[12] + CHARS[31] + CHARS[20] + CHARS[18]==350)
s.add(CHARS[27] - CHARS[23] - CHARS[0] - CHARS[4]==-206)
s.add(CHARS[15] - CHARS[16] - CHARS[18] - CHARS[10]==-80)
s.add(CHARS[29] - CHARS[22] - CHARS[1] * CHARS[12]==-11870)
s.add(CHARS[16] * CHARS[25] - CHARS[21] + CHARS[24]==10204)
s.add(CHARS[17] + CHARS[3] + CHARS[14] - CHARS[14]==226)
s.add(CHARS[4] + CHARS[17] - CHARS[7] + CHARS[15]==248)
s.add(CHARS[12] * CHARS[13]==9595)
s.add(CHARS[29] - CHARS[14] - CHARS[6] - CHARS[8]==-95)
s.add(CHARS[1] + CHARS[0] * CHARS[29] + CHARS[23]==10214)
s.add(CHARS[26] - CHARS[12] + CHARS[6] * CHARS[31]==4846)
s.add(CHARS[31] - CHARS[24] + CHARS[27] - CHARS[25]==56)
s.add(CHARS[30] - CHARS[31] - CHARS[25] - CHARS[11]==-193)
s.add(CHARS[4] * CHARS[24] - CHARS[27] - CHARS[12]==6303)
s.add(CHARS[27] - CHARS[28] - CHARS[10] + CHARS[16]==36)
s.add(CHARS[21] - CHARS[28] - CHARS[19] - CHARS[13]==-226)
s.add(CHARS[21] + CHARS[4] - CHARS[6] + CHARS[21]==293)
s.add(CHARS[3] * CHARS[29] - CHARS[11] + CHARS[25]==12087)
s.add(CHARS[14] + CHARS[1] - CHARS[24] + CHARS[5]==224)
s.add(CHARS[18] - CHARS[29] - CHARS[7] - CHARS[23]==-239)
s.add(CHARS[7] - CHARS[2] + CHARS[10] - CHARS[4]==-87)
s.add(CHARS[3] - CHARS[5] * CHARS[8] - CHARS[14]==-10597)
s.add(CHARS[26] - CHARS[8] + CHARS[30] - CHARS[11]==-29)
s.add(CHARS[30] - CHARS[28] + CHARS[15] * CHARS[6]==5559)
s.add(CHARS[17] + CHARS[29] - CHARS[9] + CHARS[28]==220)
s.add(CHARS[15] + CHARS[2] + CHARS[5] - CHARS[16]==239)
s.add(CHARS[15] + CHARS[30] - CHARS[10] - CHARS[3]==61)
s.add(CHARS[27] + CHARS[20] - CHARS[30] + CHARS[2]==202)
s.add(CHARS[8] + CHARS[19] * CHARS[3] - CHARS[27]==14012)
s.add(CHARS[12] + CHARS[22] * CHARS[30] + CHARS[30]==6133)
s.add(CHARS[24] + CHARS[27] + CHARS[31] * CHARS[6]==5064)
s.add(CHARS[16] - CHARS[20] + CHARS[22] + CHARS[16]==146)
s.add(CHARS[16] - CHARS[26] + CHARS[0] + CHARS[30]==261)
s.add(CHARS[23] * CHARS[16] - CHARS[22] + CHARS[24]==9217)
s.add(CHARS[6] - CHARS[1] - CHARS[0] - CHARS[7]==-266)
s.add(CHARS[15] + CHARS[19] - CHARS[5] * CHARS[19]==-12419)
s.add(CHARS[0] + CHARS[13] * CHARS[14] + CHARS[6]==4804)
s.add(CHARS[25] + CHARS[15] + CHARS[2] + CHARS[31]==434)
s.add(CHARS[31] - CHARS[4] + CHARS[13] - CHARS[31]==-28)
s.add(CHARS[14] + CHARS[10] * CHARS[0] + CHARS[8]==5095)
s.add(CHARS[1] * CHARS[3] - CHARS[2] + CHARS[29]==14387)
s.add(CHARS[11] + CHARS[9] * CHARS[3] + CHARS[1]==13393)
s.add(CHARS[9] - CHARS[30] + CHARS[4] - CHARS[24]==62)
s.add(CHARS[26] + CHARS[15] * CHARS[7] - CHARS[28]==10946)
s.add(CHARS[7] + CHARS[7] + CHARS[14] + CHARS[26]==290)
s.add(CHARS[11] + CHARS[6] + CHARS[27] + CHARS[0]==363)
s.add(CHARS[25] - CHARS[12] + CHARS[8] + CHARS[26]==155)
s.add(CHARS[15] + CHARS[24] - CHARS[10] + CHARS[18]==172)
s.add(CHARS[27] - CHARS[21] + CHARS[8] + CHARS[17]==207)
s.add(CHARS[25] + CHARS[1] + CHARS[13] - CHARS[12]==220)
s.add(CHARS[5] - CHARS[30] + CHARS[5] - CHARS[6]==56)
s.add(CHARS[19] - CHARS[5] * CHARS[14] + CHARS[20]==-5180)

if s.check()==sat: 
    m = s.model()
    flag = ""
    for i in range(32):
        flag+=chr(int(m[CHARS[i]].as_long()))
    print(flag)
